﻿module Analysis
(*
 * Blueprint for the part where the analysis algorithm is implemented.
 *)

(************************************************************)
(* definitions of the abstract domain and its operators.    *)
(************************************************************)
module AbstractDomain = 
    type myLattice = int   
    let Bottom = 0

(************************************************************)
(* definitions of abstract states.                          *)
(************************************************************)
module AbstractSemantics = 
    type PState = AbstractDomain.myLattice array   (* an F# array type *)
    let  bottomState n = Array.create n AbstractDomain.Bottom
    (* some operations on states... *)


type resultType = 
    {
        info: int
    }
    member x.toString() = x.info.ToString()

(*  main analysis function. currently quite stupid *)
let analyse(c : Core.Cmd) : resultType = 

    let numVars = Core.highest_var c

    let rec abstractInt(c: Core.Cmd, s: AbstractSemantics.PState) : AbstractSemantics.PState =
        match c with 
                    |  Core.Seq(c1,c2)        -> [| 1; 2 |]
                    |  Core.Choice(c1,c2)     -> [| 1; 2 |]
                    |  Core.Skip              -> [| 1; 2 |]
                    |  Core.Asgn(i, e)        -> [| 1; 2 |]
                    |  Core.Loop(i, c)        -> [| 1; 2 |]
    { info = 42 } : resultType


